The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CdtProblem
↳3 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 52 ms)
↳4 CdtProblem
↳5 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CdtProblem
↳7 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 CdtProblem
↳9 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
↳10 CdtProblem
↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳12 CdtProblem
↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
↳14 CdtProblem
↳15 CdtInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳16 CdtProblem
↳17 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)
↳18 CdtProblem
↳19 CdtInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳20 CdtProblem
↳21 CdtInstantiationProof (BOTH BOUNDS(ID, ID), 0 ms)
↳22 CdtProblem
↳23 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)
↳24 CdtProblem
↳25 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 12 ms)
↳26 CdtProblem
↳27 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳28 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

f(x, c(y)) → f(x, s(f(y, y)))
f(s(x), y) → f(x, s(c(y)))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1))
F(s(z0), z1) → c2(F(z0, s(c(z1))))
S tuples:

F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1))
F(s(z0), z1) → c2(F(z0, s(c(z1))))
K tuples:none
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c2

(3) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1))
We considered the (Usable) Rules:none
And the Tuples:

F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1))
F(s(z0), z1) → c2(F(z0, s(c(z1))))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F(x1, x2)) = x2   
POL(c(x1)) = [1] + x1   
POL(c1(x1, x2)) = x1 + x2   
POL(c2(x1)) = x1   
POL(f(x1, x2)) = x2   
POL(s(x1)) = 0   

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1))
F(s(z0), z1) → c2(F(z0, s(c(z1))))
S tuples:

F(s(z0), z1) → c2(F(z0, s(c(z1))))
K tuples:

F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c1, c2

(5) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1)) by

F(z0, c(c(y1))) → c1(F(z0, s(f(c(y1), c(y1)))), F(c(y1), c(y1)))
F(s(y0), c(z1)) → c1(F(s(y0), s(f(z1, z1))), F(z1, z1))
F(z0, c(s(y0))) → c1(F(z0, s(f(s(y0), s(y0)))), F(s(y0), s(y0)))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(s(z0), z1) → c2(F(z0, s(c(z1))))
F(z0, c(c(y1))) → c1(F(z0, s(f(c(y1), c(y1)))), F(c(y1), c(y1)))
F(s(y0), c(z1)) → c1(F(s(y0), s(f(z1, z1))), F(z1, z1))
F(z0, c(s(y0))) → c1(F(z0, s(f(s(y0), s(y0)))), F(s(y0), s(y0)))
S tuples:

F(s(z0), z1) → c2(F(z0, s(c(z1))))
K tuples:

F(z0, c(c(y1))) → c1(F(z0, s(f(c(y1), c(y1)))), F(c(y1), c(y1)))
F(s(y0), c(z1)) → c1(F(s(y0), s(f(z1, z1))), F(z1, z1))
F(z0, c(s(y0))) → c1(F(z0, s(f(s(y0), s(y0)))), F(s(y0), s(y0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1

(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(s(z0), z1) → c2(F(z0, s(c(z1))))
F(z0, c(c(y1))) → c1(F(z0, s(f(c(y1), c(y1)))), F(c(y1), c(y1)))
F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(s(y0), c(z1)) → c3(F(z1, z1))
F(z0, c(s(y0))) → c3(F(z0, s(f(s(y0), s(y0)))))
F(z0, c(s(y0))) → c3(F(s(y0), s(y0)))
S tuples:

F(s(z0), z1) → c2(F(z0, s(c(z1))))
K tuples:

F(z0, c(c(y1))) → c1(F(z0, s(f(c(y1), c(y1)))), F(c(y1), c(y1)))
F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(s(y0), c(z1)) → c3(F(z1, z1))
F(z0, c(s(y0))) → c3(F(z0, s(f(s(y0), s(y0)))))
F(z0, c(s(y0))) → c3(F(s(y0), s(y0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1, c3

(9) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

F(s(y0), c(z1)) → c3(F(z1, z1))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(s(z0), z1) → c2(F(z0, s(c(z1))))
F(z0, c(c(y1))) → c1(F(z0, s(f(c(y1), c(y1)))), F(c(y1), c(y1)))
F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(z0, c(s(y0))) → c3(F(z0, s(f(s(y0), s(y0)))))
F(z0, c(s(y0))) → c3(F(s(y0), s(y0)))
S tuples:

F(s(z0), z1) → c2(F(z0, s(c(z1))))
K tuples:

F(z0, c(c(y1))) → c1(F(z0, s(f(c(y1), c(y1)))), F(c(y1), c(y1)))
F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(z0, c(s(y0))) → c3(F(z0, s(f(s(y0), s(y0)))))
F(z0, c(s(y0))) → c3(F(s(y0), s(y0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c1, c3

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(z0, c(c(y1))) → c1(F(z0, s(f(c(y1), c(y1)))), F(c(y1), c(y1))) by

F(x0, c(c(z1))) → c1(F(x0, s(f(c(z1), s(f(z1, z1))))), F(c(z1), c(z1)))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(s(z0), z1) → c2(F(z0, s(c(z1))))
F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(z0, c(s(y0))) → c3(F(z0, s(f(s(y0), s(y0)))))
F(z0, c(s(y0))) → c3(F(s(y0), s(y0)))
F(x0, c(c(z1))) → c1(F(x0, s(f(c(z1), s(f(z1, z1))))), F(c(z1), c(z1)))
S tuples:

F(s(z0), z1) → c2(F(z0, s(c(z1))))
K tuples:

F(z0, c(c(y1))) → c1(F(z0, s(f(c(y1), c(y1)))), F(c(y1), c(y1)))
F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(z0, c(s(y0))) → c3(F(z0, s(f(s(y0), s(y0)))))
F(z0, c(s(y0))) → c3(F(s(y0), s(y0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c1

(13) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(z0, c(s(y0))) → c3(F(z0, s(f(s(y0), s(y0))))) by

F(x0, c(s(z0))) → c3(F(x0, s(f(z0, s(c(s(z0)))))))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(s(z0), z1) → c2(F(z0, s(c(z1))))
F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(z0, c(s(y0))) → c3(F(s(y0), s(y0)))
F(x0, c(c(z1))) → c1(F(x0, s(f(c(z1), s(f(z1, z1))))), F(c(z1), c(z1)))
F(x0, c(s(z0))) → c3(F(x0, s(f(z0, s(c(s(z0)))))))
S tuples:

F(s(z0), z1) → c2(F(z0, s(c(z1))))
K tuples:

F(z0, c(c(y1))) → c1(F(z0, s(f(c(y1), c(y1)))), F(c(y1), c(y1)))
F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(z0, c(s(y0))) → c3(F(z0, s(f(s(y0), s(y0)))))
F(z0, c(s(y0))) → c3(F(s(y0), s(y0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c2, c3, c1

(15) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace F(s(z0), z1) → c2(F(z0, s(c(z1)))) by

F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
F1(s(z0), z1) → c2(F(z0, s(c(z1))))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(z0, c(s(y0))) → c3(F(s(y0), s(y0)))
F(x0, c(c(z1))) → c1(F(x0, s(f(c(z1), s(f(z1, z1))))), F(c(z1), c(z1)))
F(x0, c(s(z0))) → c3(F(x0, s(f(z0, s(c(s(z0)))))))
F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
F1(s(z0), z1) → c2(F(z0, s(c(z1))))
S tuples:

F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
F1(s(z0), z1) → c2(F(z0, s(c(z1))))
K tuples:

F(z0, c(c(y1))) → c1(F(z0, s(f(c(y1), c(y1)))), F(c(y1), c(y1)))
F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(z0, c(s(y0))) → c3(F(z0, s(f(s(y0), s(y0)))))
F(z0, c(s(y0))) → c3(F(s(y0), s(y0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F, F1

Compound Symbols:

c3, c1, c2

(17) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

F1(s(z0), z1) → c2(F(z0, s(c(z1))))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(z0, c(s(y0))) → c3(F(s(y0), s(y0)))
F(x0, c(c(z1))) → c1(F(x0, s(f(c(z1), s(f(z1, z1))))), F(c(z1), c(z1)))
F(x0, c(s(z0))) → c3(F(x0, s(f(z0, s(c(s(z0)))))))
F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
S tuples:

F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
K tuples:

F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(z0, c(s(y0))) → c3(F(s(y0), s(y0)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c1, c2

(19) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace F(z0, c(s(y0))) → c3(F(s(y0), s(y0))) by

F(c(s(z1)), c(s(z1))) → c3(F(s(z1), s(z1)))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(x0, c(c(z1))) → c1(F(x0, s(f(c(z1), s(f(z1, z1))))), F(c(z1), c(z1)))
F(x0, c(s(z0))) → c3(F(x0, s(f(z0, s(c(s(z0)))))))
F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
F(c(s(z1)), c(s(z1))) → c3(F(s(z1), s(z1)))
S tuples:

F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
K tuples:

F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(c(s(z1)), c(s(z1))) → c3(F(s(z1), s(z1)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c1, c2

(21) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use instantiation to replace F(x0, c(c(z1))) → c1(F(x0, s(f(c(z1), s(f(z1, z1))))), F(c(z1), c(z1))) by

F(c(c(z1)), c(c(z1))) → c1(F(c(c(z1)), s(f(c(z1), s(f(z1, z1))))), F(c(z1), c(z1)))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(x0, c(s(z0))) → c3(F(x0, s(f(z0, s(c(s(z0)))))))
F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
F(c(s(z1)), c(s(z1))) → c3(F(s(z1), s(z1)))
F(c(c(z1)), c(c(z1))) → c1(F(c(c(z1)), s(f(c(z1), s(f(z1, z1))))), F(c(z1), c(z1)))
S tuples:

F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
K tuples:

F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(c(s(z1)), c(s(z1))) → c3(F(s(z1), s(z1)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c2, c1

(23) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(x0, c(s(z0))) → c3(F(x0, s(f(z0, s(c(s(z0)))))))
F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
F(c(s(z1)), c(s(z1))) → c3(F(s(z1), s(z1)))
F(c(c(z1)), c(c(z1))) → c1(F(c(z1), c(z1)))
S tuples:

F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
K tuples:

F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(c(s(z1)), c(s(z1))) → c3(F(s(z1), s(z1)))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c2, c1

(25) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
We considered the (Usable) Rules:none
And the Tuples:

F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(x0, c(s(z0))) → c3(F(x0, s(f(z0, s(c(s(z0)))))))
F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
F(c(s(z1)), c(s(z1))) → c3(F(s(z1), s(z1)))
F(c(c(z1)), c(c(z1))) → c1(F(c(z1), c(z1)))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F(x1, x2)) = x1   
POL(c(x1)) = x1   
POL(c1(x1)) = x1   
POL(c2(x1)) = x1   
POL(c3(x1)) = x1   
POL(f(x1, x2)) = 0   
POL(s(x1)) = [1] + x1   

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, c(z1)) → f(z0, s(f(z1, z1)))
f(s(z0), z1) → f(z0, s(c(z1)))
Tuples:

F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(x0, c(s(z0))) → c3(F(x0, s(f(z0, s(c(s(z0)))))))
F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
F(c(s(z1)), c(s(z1))) → c3(F(s(z1), s(z1)))
F(c(c(z1)), c(c(z1))) → c1(F(c(z1), c(z1)))
S tuples:none
K tuples:

F(s(y0), c(z1)) → c3(F(s(y0), s(f(z1, z1))))
F(c(s(z1)), c(s(z1))) → c3(F(s(z1), s(z1)))
F(s(z0), s(c(x1))) → c2(F(z0, s(c(s(c(x1))))))
F(s(x0), s(y0)) → c2(F(x0, s(c(s(y0)))))
F(s(x1), s(x1)) → c2(F(x1, s(c(s(x1)))))
F(s(z0), s(f(c(x1), s(y0)))) → c2(F(z0, s(c(s(f(c(x1), s(y0)))))))
Defined Rule Symbols:

f

Defined Pair Symbols:

F

Compound Symbols:

c3, c2, c1

(27) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(28) BOUNDS(1, 1)